Library iso_conjugate

Require Import PointsETC.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition iso_conjugate P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  cTriple (q×r×v×w) (r×p×w×u) (p×q×u×v)
 end.

Lemma X1_iso_conjugate_of_X2_X6 :
 eq_points X_1 (iso_conjugate X_2 X_6).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.

End Triangle.